Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are widely used in automated verification, but there is a lack of interactive tools designed for educational purposes in this field. To address this gap, we present EduSAT, a pedagogical tool specifically developed to support learning and understanding of SAT and SMT solving. EduSAT offers implementations of key algorithms such as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and the Reduced Order Binary Decision Diagram (ROBDD) for SAT solving. Additionally, EduSAT provides solver abstractions for five NP-complete problems beyond SAT and SMT. Users can benefit from EduSAT by experimenting, analyzing, and validating their understanding of SAT and SMT solving techniques. Our tool is accompanied by comprehensive documentation and tutorials, extensive testing, and practical features such as a natural language interface and SAT and SMT formula generators, which also serve as a valuable opportunity for learners to deepen their understanding. Our evaluation of EduSAT demonstrates its high accuracy, achieving 100% correctness across all the implemented SAT and SMT solvers. We release EduSAT as a python package in .whl file, and the source can be identified at https://github.com/zhaoy37/SAT_Solver.

Success! Now check your email to confirm your subscription. There was an error submitting your subscription.

One of the more important aims of graduate artificial intelligence courses is to prepare graduate students to critically evaluate the current literature. The established approaches for this include either asking a student to present a paper in class, or to have the entire class read and discuss a paper. However, neither of these approaches presents incentives for student participation beyond the posting of a single summary or review. In this paper, we describe a class project that uses the popular Easychair conference management system as a pedagogical tool to enable engagement in the peer review process. We report on the deployment of this project in a medium-sized graduate AI class, and present the results of this deployment. We hope that the success of this project in engaging students in the peer review process can be used better train and bolster the future corps of AI reviewers.

This paper intends to demonstrate how Applicative and Combinatory Categorial Grammar (ACCG) can be drawn on to design powerful software applications for the teaching of languages. To this end, we present some modules from our “pictographic translator”, a software that performs syntactical analysis of sentences in natural language directly written by the user, and then dynamically displays series of pictograms that illustrate the words and structure of the user’s sentences. After a short presentation of our application and an introduction to ACCG, we will examine how this formalism enables the building of several high-level functions in our system, such as disambiguation, structure exhibition and grammatical correction/validation. We finally open a short discussion concerning the potential (and limits) of this architecture with regards to multilingualism.